/*
 * WatchedClausesListTester.cuh
 *
 *  Created on: Oct 24, 2013
 *      Author: jaime
 */

#ifndef WATCHEDCLAUSESLISTTESTER_CUH_
#define WATCHEDCLAUSESLISTTESTER_CUH_

#include "../../BCPStrategy/WatchedClausesList.cuh"
#include "../../SATSolver/VariablesStateHandler.cuh"
#include "../../Utils/CUDAClauseVec.cuh"
#include "../../Utils/GPULinkedList.cuh"
#include "../../Utils/GPUStaticVec.cuh"
#include "../../SATSolver/SolverTypes.cuh"
#include "../Tester.cuh"

class WatchedClausesListTester : public Tester {
private:
	WatchedClausesList watched_clauses_list;
	VariablesStateHandler handler;
	CUDAClauseVec * formula;
	GPUStaticVec<Lit> assumptions;

public:
	__device__ bool test_implication_from_clauses();


	__device__ WatchedClausesListTester(DataToDevice & data);
	__device__ void test_all();
};

#endif /* WATCHEDCLAUSESLISTTESTER_CUH_ */
